|
In computer science, type safety is the extent to which a programming language discourages or prevents type errors. A type error is erroneous or undesirable program behaviour caused by a discrepancy between differing data types for the program's constants, variables, and methods (functions), e.g., treating an integer (int) as a floating-point number (float). Type safety is sometimes alternatively considered to be a property of a computer program rather than the language in which that program is written; that is, some languages have type-safe facilities that can be circumvented by programmers who adopt practices that exhibit poor type safety. The formal type-theoretic definition of type safety is considerably stronger than what is understood by most programmers. Type enforcement can be static, catching potential errors at compile time, or dynamic, associating type information with values at run-time and consulting them as needed to detect imminent errors, or a combination of both. The behaviors classified as type errors by a given programming language are usually those that result from attempts to perform operations on values that are not of the appropriate data type. This classification is partly based on opinion; it may imply that any operation not leading to program crashes, security flaws or other obvious failures is legitimate and need not be considered an error, or it may imply that any contravention of the programmer's explicit intent (as communicated via typing annotations) to be erroneous and not "type-safe". In the context of static (compile-time) type systems, type safety usually involves (among other things) a guarantee that the eventual value of any expression will be a legitimate member of that expression's static type. The precise requirement is more subtle than this — see, for example, subtype and polymorphism for complications. Type safety is closely linked to ''memory safety'', a restriction on the ability to copy arbitrary bit patterns from one memory location to another. For instance, in an implementation of a language that has some type , such that some sequence of bits (of the appropriate length) does not represent a legitimate member of , if that language allows data to be copied into a variable of type , then it is not type-safe because such an operation might assign a non- value to that variable. Conversely, if the language is type-unsafe to the extent of allowing an arbitrary integer to be used as a pointer, then it is not memory-safe. Most statically typed languages provide a degree of type safety that is strictly stronger than memory safety, because their type systems enforce the proper use of abstract data types defined by programmers even when this is not strictly necessary for memory safety or for the prevention of any kind of catastrophic failure. ==Definitions== Type-safe code accesses only the memory locations it is authorized to access. (For this discussion, type safety specifically refers to memory type safety and should not be confused with type safety in a broader respect.) For example, type-safe code cannot read values from another object's private fields. Robin Milner provided the following slogan to describe type safety: :Well-typed programs cannot "go wrong". The appropriate formalization of this slogan depends on the style of formal semantics used for a particular language. In the context of denotational semantics, type safety means that the value of an expression that is well-typed, say with type τ, is a ''bona fide'' member of the set corresponding to τ. In 1994, Andrew Wright and Matthias Felleisen formulated what is now the standard definition and proof technique for type safety in languages defined by operational semantics. Under this approach, type safety is determined by two properties of the semantics of the programming language: ;(Type-) preservation or subject reduction: "Well typedness" of programs remains invariant under the transition rules (i.e. evaluation rules or reduction rules) of the language. ;Progress: A well typed program never gets "stuck", i.e., never gets into an undefined state where no further transitions are possible. These properties do not exist in a vacuum; they are linked to the semantics of the programming language they describe, and there is a large space of varied languages that can fit these criteria, since the notion of "well typed" program is part of the static semantics of the programming language and the notion of "getting stuck" (or "going wrong") is a property of its dynamic semantics. Vijay Saraswat provides the following definition: :"A language is type-safe if the only operations that can be performed on data in the language are those sanctioned by the type of the data." 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Type safety」の詳細全文を読む スポンサード リンク
|